modality (圈)
modality in nLab
Modalities — Agda 2.8.0 documentation
冪等 monad の事
Francis William Lawvere "Some Thoughts on the Future of Category Theory" 1991
modal type theory in nLab
modal type in nLab
comodal type in nLab
possibility$ \lozenge$ \dashvnecessity$ \square
necessity and possibility in nLab
dR-shape modality$ \int_{\rm dR}$ \dashvdR-flat modality$ \flat_{\rm dR}
dR-shape modality in nLab
dR-flat modality in nLab
reduction modality$ \frak R$ \dashvinfinitesimal shape modality$ \frak F$ \dashvinfinitesimal flat modality$ \&
reduction modality in nLab
infinitesimal shape modality in nLab
infinitesimal flat modality in nLab
fermionic modality$ \rightrightarrows$ \dashvbosonic modality$ \rightsquigarrow$ \dashvrheonomy modality$ \rm Rh
bosonic modality in nLab
rheonomy modality in nLab
classical modality$ \natural
classical modality in nLab
Polarity Annotations — Agda 2.8.0 documentation#The polarity modality Agda implements polarity annotations usin
Generalization of Declared Variables — Agda 2.8.0 documentation#Modalities One can give a modality when declaring a generalizab
Cubical — Agda 2.8.0 documentation#Modalities & indexed matching When using indexed matching in Cu
立方體的集合
圏論的モダリティ:圏上の非自然な構造達 - 檜山正幸のキマイラ飼育記 (はてなBlog)
非全域関手と非自然変換 - 檜山正幸のキマイラ飼育記 (はてなBlog)
余可換コモノイド・モダリティ事件の解説 - 檜山正幸のキマイラ飼育記 (はてなBlog)
この記事では
部分函手 (partial functor)
partial functor in nLab
圈$ \bf C,$ \bf Dに對して、部分寫像$ F^{\rm obj}:|{\bf C}|\to|{\bf D}|と部分寫像$ F^{\rm mor}:{\rm Hom}_{\bf C}\to{\rm Hom}_{\bf D}の組$ F:=(F^{\rm obj},F^{\rm mor})で以下を滿たすものを部分函手$ F:{\bf C}\to{\bf D}と呼ぶ
※$ F^{\rm mor}の域を$ {\bf C}(A,B)の部分集合に制限した部分寫像を$ {F^{\rm mor}}_{A,B}と書く
$ F^{\rm obj}の域に對象$ A,B\in|{\bf C}|が含まれてゐるならば、部分寫像$ {F^{\rm mor}}_{A,B}:{\bf C}(A,B)\to{\bf D}(F^{\rm obj}(A),F^{\rm obj}(B))が定義されてゐる
$ F^{\rm obj}の域に對象$ A\in|{\bf C}|が含まれてゐるならば、恆等射$ {\rm id}_Aは$ {F^{\rm mor}}_{A,A}の域に含まれてゐる
合成射を保つ。射$ f:A\to B,$ g:B\to Cに對して$ {F^{\rm mor}}_{A,C}(f;g)={F^{\rm mor}}_{A,B}(f);{F^{\rm mor}}_{B,C}(g)
恆等射を保つ$ {F^{\rm mor}}_{A,A}({\rm id}_A)={\rm id}_{F^{\rm obj}(A)}
非自然變換 (non-natural transformation)
unnatural transformation in nLab
部分函手$ F,G:{\bf C}\to{\bf D}に對して、部分寫像$ \alpha:|{\bf C}|\to{\rm Hom}_{\bf D}で以下を滿たすものを非自然變換$ \alpha:F\Rarr G,A\mapsto\alpha_Aと呼ぶ
$ \alpha_Aが定義されてゐる ($ \alphaの域に對象$ A\in|{\bf C}|が含まれてゐる) ならば、$ Aは$ Fの域にも$ Gの域にも含まれてゐる
$ \alpha_Aは射$ F(A)\to G(A)である
非自然變換の組を modality (圈) と呼ぶ
非自然變換に整合する (consistent。compatible) 射
部分函手$ F,G:{\bf C}\to{\bf D}と非自然變換$ \alpha:F\Rarr Gに對して、$ {\bf C}での射$ f:A\to Bは、可換圖式$ F(A)\xrightarrow{\alpha_A}G(A)\xrightarrow{G(f)}G(B)\xleftarrow{\alpha_B}F(B)\xleftarrow{F(f)}F(A)を滿たせば非自然變換$ \alphaに整合すると言ふ
非自然變換に整合する射の全體は、$ {\bf D}の部分圈を成す
例
$ \bf Setの附點 modality (pointed-set modality)
單集合 (singleton)$ 1=\{*\}から$ \bf Setの全ての對象への射の族$ \theta:=\{\theta_X:1\to X|X\in|{\bf Set}|\}を附點 modality (pointed-set modality) と呼ぶ。函手$ 1:{\bf Set}\to\{1\}から函手$ {\rm Id}:{\bf Set}\to{\bf Set}への全域な非自然變換$ \theta:|{\bf Set}|\to{\rm Hom}_{\bf Set}と見做せる
附點 modality が自然變換$ 1\Rarr{\rm Id},$ 1\xrightarrow{\theta_X}X\xrightarrow{f}Y\xleftarrow{\theta_Y}1\xleftarrow{}1と成る樣な射$ fを、$ \thetaと整合する射と呼ぶ
整合する射の全體は$ {\bf Set}の部分圈を成す。全ての集合になんらかの附點をつけた圈に成る
餘可換餘 monoid modality (cocommutative comonoid modality)
對稱 monoidal 圈$ ({\bf C},\otimes,1,\alpha,\lambda,\rho,\sigma)に對して、全域な非自然變換$ \Delta,\epsilon:|{\bf C}|\to{\rm Hom}_{\bf C},$ \Delta_X:X\to X\otimes X,$ \epsilon_X:X\to 1の組$ (\Delta,\epsilon)は以下を滿たせば餘可換餘 monoid modality と呼ぶ
($ \Delta_Xは餘乘法として、$ \epsilon_Xは餘單位として振る舞ふ)
餘結合律$ \Delta_X;(\Delta_X\otimes{\rm id}_X)=\Delta_X(X\otimes\Delta_X)
左餘單位律$ \Delta_X;(\epsilon_X\otimes{\rm id}_X)={\rm id}_X
右餘單位律$ \Delta_X;({\rm id}_X\otimes\epsilon_X)={\rm id}_X
餘可換律$ \Delta_X;\sigma_X=\Delta_X